00100	
00110	(DE RESOLV(C D)
00120	(COND((AND(ALLPOS C)(ALLPOS D))NIL)
00130	      ((AND(ALLNEG C)(ALLNEG D))NIL)
00135	((NOT(HERE C)) NIL)((NOT(HERE D))NIL)
00140	(T(RESOLVE C D))) )
00150	
00200	
00300	(DEFPROP RESOLVEL 
00400	 (LAMBDA(C D)
00500	  (PROG (Z)
00550	(SETQ Z1 C)
00600	A
00650	    (SETQ Z (RESOLV C (CAR D)))
00700		(COND (Z (RETURN Z)))
00800	B	(SETQ D (CDR D))
00900		(COND (D (SETQ Z2(CAR D))(GO A)))
01000		(RETURN NIL))) 
01100	EXPR)
01200	
01300	(DEFPROP UNITUNITRES 
01400	 (LAMBDA(L R)
01500	  (PROG (L1 Z)
01550	(COND((NULL L)(RETURN NIL)))(SETQ L1 L)
01600	A
01650	    (COND ((RESOLV (CAR L1) (CAR R)) (RETURN (CONS (CAR L1) (CAR R)))))
01700	B	(SETQ L1 (CDR L1))
01800		(COND (L1 (GO A)))
01900		(SETQ R (CDR R))
02000		(COND (R (SETQ L1 L) (GO A)))
02100		(RETURN NIL))) 
02200	EXPR)
02300	
02400	(DEFPROP SPLITEM 
02500	 (LAMBDA(L)
02600	  (PROG (U NU)
02700	   A    (COND ((EQ (LENGTH (CDAR L)) 1) (SETQ U (CONS (CAR L) U))) (T (SETQ NU (CONS (CAR L) NU))))
02800		(SETQ L (CDR L))
02900		(COND (L (GO A)) (T (RETURN (CONS U NU)))))) 
03000	EXPR)
03100	
03200	(DEFPROP UNITRES1 
03300	 (LAMBDA(C US)
03400	  (PROG (R)
03500		(SETQ Z1 C)
03600	   A    (SETQ Z2 (CAR US))
03700		(SETQ R (APPEND R (RESOLV Z1 Z2)))
03800	B	(SETQ US (CDR US))
03900		(COND (US (GO A)))
04000		(RETURN R))) 
04100	EXPR)
04200	
04300	(DEFPROP TRYPRF 
04400	 (LAMBDA(L)
04500	  (PROG (U A C FLG R Z1 Z2 Z CNT )(SETQ CNT 0)
04600		(SETQ Z (SPLITEM L))
04700		(SETQ U (CAR Z))
04800		(SETQ A (CDR Z))
04900		(SETQ C NIL)
05000		(SETQ FLG NIL)
05100	   A    (COND ((NULL (SETQ R (UNITRES1 (CAR A) U))) (SETQ C (APPEND C (LIST (CAR A)))) (SETQ A (CDR A)) (GO B))
05200		      ((MEMQ NIL R) (PROOF Z1 Z2) (RETURN (QUOTE QED))))
05300		(SETQ R (FINI L R Z1 Z2 EE1))
05350	(SETQ CNT(PLUS CNT(LENGTH R)))
05400		(COND ((NULL R) (SETQ C (APPEND C (LIST (CAR A)))) (SETQ A (CDR A)) (GO B)))
05500		(SETQ Z (SPLITEM R))
05600		(COND ((SETQ R (UNITUNITRES (CAR Z) U)) (PROOF (CAR R) (CDR R)) (RETURN (QUOTE QED))))
05700		(SETQ U (APPEND U (CAR Z)))
05800		(SETQ A (APPEND (CDR Z) (CDR A)(LIST(CAR A))))
05900	   B(COND((TTYIN)(UPDATE CLAUSES)))
05950	    (COND (A (GO A)) ((NULL FLG) (SETQ A C) (SETQ C NIL) (SETQ FLG T) (GO A)))
06000		(SETQ FLG NIL)
06100		(SETQ C1 (REVERSE C))
06200	   C    (SETQ Z (RESOLVEL (CAR C1) C))
06300		(COND ((NULL Z) (GO C1)))
06400		(SETQ Z (FINI L Z Z1 Z2 EE1))
06450	(SETQ CNT(PLUS CNT(LENGTH Z)))
06500		(COND ((NULL Z) (GO C1)))
06600		(SETQ A (APPEND Z (CDR C) (LIST (CAR C))))
06700		(SETQ C NIL)
06800		(GO A)
06900	   C1   (SETQ C1 (CDR C1))
07000		(COND (C1 (GO C)))
07100		(PRINT (QUOTE LOSE)))) 
07200	EXPR)
07300	
07400	(DEFPROP FINI 
07500	 (LAMBDA(U R Z1 Z2 E)
07600	  (PROG (Z)
07700		(COND (UFLG (SETQ R (UNITREDUCT R UNAXP UNAXN))))
07800		(COND ((NULL R) (RETURN NIL)) ((NULL (CAR R)) (PROOF Z1 Z2) (ERR (QUOTE (QED)))))
07900		(SETQ COUNT (PLUS COUNT (LENGTH R)))
08000		(SETQ R (EDIT U R))
08100		(CLAUSES2 R)
08200		(COND ((NULL R) (RETURN NIL)))
08300		(BAKSUB CLAUSES R)
08400		(BOOKEEP E R (CONS Z1 Z2))
08500		(SETQ Z (UNITPN R))
08600		(SETQ UNAXP (APPEND (CAR Z) UNAXP))
08700		(SETQ UNAXN (APPEND (CDR Z) UNAXN))
08800	(RETURN R)))
08900	EXPR)
09000	
09100	(DEFPROP AUTO 
09200	 (LAMBDA(XX)
09300	  (PROG (X1 Z2 D M STRATEGY SUPPORT EDITSTRAT MERGE ORDER DEBUG ANCESTRY PMODEL NMODEL PFLG PDEPTH DLIST)
09400		(COND (EQUAL (SETQ PFLG NIL)) (T (SETQ PFLG NIL)))
09500		(SETQ PDEPTH 101)
09600		(SETQ DDEPTH 1)
09700		(COND
09800		 ((NULL EQUAL) (PRINT (QUOTE (IS THERE AN EQUALITY PREDICATE (Y / N))))
09900			       (COND
10000				((EQ (READ) (QUOTE Y)) (PRINT (QUOTE (WHAT IS IT)))
10100						       (SETQ PFLG NIL)
10200						       (SETQ EQUAL (READ))))))
10300		(SETQ X1 XX)
10400		(SETQ M (SETQ D 0))
10500	   A    (SETQ M (MAX M (LENGTH (CDAR X1))))
10600		(SETQ D (MAX D (DEPTH (CDAR X1))))
10700		(SETQ Z2 (CAR X1))
10800		(COND
10900		 ((AND (EQ (LENGTH (CDR Z2)) 1) (EQ (CAADR Z2) EQUAL) (NOT (EQ (CADADR Z2) (CAR (CDDADR Z2)))))
11000		  (SETQ DLIST (CONS (CONS (CONS (CAAAR Z2) (CDAR Z2)) (CDR Z2)) DLIST))))
11100		(SETQ X1 (CDR X1))
11200		(COND ((CDR X1) (GO A)))
11300		(SETQ Z2 (ASSOC (QUOTE THEOREM) NEWNAME))
11400		(COND ((NULL Z2) (GO C)) (T (SETQ Z2 (CDR Z2))))
11500	   B    (COND (Z2 (SETQ SUPPORT (CONS (CDAR Z2) SUPPORT)) (SETQ Z2 (CDR Z2)) (GO B)))
11600	   C    (COND ((NULL LENGTH) (SETQ LENGTH (DIFFERENCE (PLUS M (LENGTH (CDAR X1))) 2)))
11700		      ((ZEROP ITER) (SETQ LENGTH (ADD1 LENGTH))))
11800		(COND ((NOT (GREATERP LENGTH 0)) (SETQ LENGTH 1)))
11900		(COND ((NULL DEPTH) (SETQ DEPTH (ADD1 D))) ((NOT (ZEROP ITER)) (SETQ DEPTH (ADD1 DEPTH))))
12000		(COND ((ZEROP ITER) (SETQ ITER 1)) (T (SETQ ITER 0)))
12100	(SETQ STRATEGY NIL)(SETQ DEPTH 4)
12200		(SETQ EDITSTRAT
12300		      (QUOTE (LAMBDA (C) (OR (GREATERP (LENGTH (CDR C)) LENGTH) (GREATERP (DEPTH (CDR C)) DEPTH)))))
12400		(SETQ DEBUG T)
12500		(SETQ DLIST NIL)
12600		(RETURN
12700		 (LIST STRATEGY
12800	 	       SUPPORT
12900	 	       EDITSTRAT
13000	 	       MERGE
13100	 	       ORDER
13200	 	       DEBUG
13300	 	       DEPTH
13400	 	       LENGTH
13500	 	       ANCESTRY
13600	 	       PMODEL
13700	 	       NMODEL
13800	 	       PFLG
13900	 	       EQUAL
14000	 	       PDEPTH
14100	 	       DLIST)))) 
14200	EXPR)